n:. ||upto(n)|| ~ n 

latex

Definitions	x:A. B(x), ||as||, upto(n), t  T, Y, if b then t else f fi , (i = j), tt, P  Q, i  j , A  B, A, False, , ff, SQType(T), {T}, , S  T, P  Q, P  Q, P & Q, t  ...$L, , Unit, {i..j},
Lemmas	nat wf, nat properties, ge wf, eq int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, length wf1, append wf, upto wf, le wf, int seg wf, length append, length nil, length cons, non neg length